A:Type, f:a:A fp Top, eq:EqDecider(A), x:A. x  dom(f)  (x  fpf-domain(f)) 

latex

Definitions	EqDecider(T), x. t(x), Top, a:A fp B(a), x  dom(f), fpf-domain(f), Prop, b, deq-member(eq;x;L), P  Q, P & Q, P  Q, P  Q, (x  l), x:A. B(x), t  T
Lemmas	l member wf, deq-member wf, assert wf, assert-deq-member, iff functionality wrt iff, top wf, fpf wf, deq wf